Termination Proof Script
Consider the TRS R consisting of the rewrite rule
1:
and
(
not
(
not
(x)),y,
not
(z))
→
and
(y,
band
(x,z),x)
There is one dependency pair:
2:
AND
(
not
(
not
(x)),y,
not
(z))
→
AND
(y,
band
(x,z),x)
The approximated dependency graph contains one SCC: {2}.
Consider the SCC {2}. There are no usable rules.
The constraints could not be solved.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006